DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2010.13

Special tree-width and the verification of monadic second-order graph pr operties

Authors: Bruno Courcelle

Published in: LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

Abstract

The model-checking problem for monadic second-order logic on graphs is fixed-parameter tractable with respect to tree-width and clique-width. The proof constructs finite deterministic automata from monadic second-order sentences, but this computation produces automata of hyper-exponential sizes, and this is not avoidable. To overcome this difficulty, we propose to consider particular monadic second-order graph properties that are nevertheless interesting for Graph Theory and to interpret automata instead of trying to compile them (joint work with I. Durand). For checking monadic second-order sentences written with edge set quantifications, the appropriate parameter is tree-width. We introduce special tree-width, a graph complexity measure between path-width and tree-width. The corresponding automata are easier to construct than those for tree-width.

Cite as

Bruno Courcelle. Special tree-width and the verification of monadic second-order graph pr operties. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 13-29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{courcelle:LIPIcs.FSTTCS.2010.13,
  author =	{Courcelle, Bruno},
  title =	{{Special tree-width and the verification of monadic second-order graph pr operties}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{13--29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.13},
  URN =		{urn:nbn:de:0030-drops-28494},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.13},
  annote =	{Keywords: model-checking, monadic second-order logic, fixed-parameter tractability, special tree-width}
}

Document

DOI: 10.4230/DagSemRep.53

Graph-Transformations in Computer Science (Dagstuhl Seminar 9301)

Authors: Bruno Courcelle, Hartmut Ehrig, Grzegorz Rozenberg, and Hans Jürgen Schneider

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract

Cite as

Bruno Courcelle, Hartmut Ehrig, Grzegorz Rozenberg, and Hans Jürgen Schneider. Graph-Transformations in Computer Science (Dagstuhl Seminar 9301). Dagstuhl Seminar Report 53, pp. 1-32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1992)

Copy BibTex To Clipboard

@TechReport{courcelle_et_al:DagSemRep.53,
  author =	{Courcelle, Bruno and Ehrig, Hartmut and Rozenberg, Grzegorz and Schneider, Hans J\"{u}rgen},
  title =	{{Graph-Transformations in Computer Science (Dagstuhl Seminar 9301)}},
  pages =	{1--32},
  ISSN =	{1619-0203},
  year =	{1992},
  type = 	{Dagstuhl Seminar Report},
  number =	{53},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemRep.53},
  URN =		{urn:nbn:de:0030-drops-149411},
  doi =		{10.4230/DagSemRep.53},
}

Search Results

Documents authored by Courcelle, Bruno

Special tree-width and the verification of monadic second-order graph pr operties

Abstract

Cite as

Graph-Transformations in Computer Science (Dagstuhl Seminar 9301)

Abstract

Cite as

Thanks for your feedback!

Could not send message